(declare-fun a () (Array Int Int))
(declare-fun b () (Array Int Int))
(declare-fun c () (Array Int Int))
(declare-fun d () (Array Int Int))
(declare-fun e () (Array Int Int))
(declare-fun f () (Array Int Int))
(declare-fun n () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun l () (Array Int Int))
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun o () Int)
(declare-fun m ((Array Int Int) (Array Int Int)) Int)
(assert (= (store l k n) (store b k i)))
(assert (= c d (store a j h)))
(assert (distinct e (store d o g)))
(assert (= n (select a j)))
(assert (distinct h (select a o) (select b o)))
(assert (= k (select e (m c f))))
(check-sat)
